Nuprl Lemma : sorted-cons
0,22
postcript
pdf
T
:Type.
T
(
x
:
T
,
L
:
T
List. sorted(
x
.
L
)
sorted(
L
) & (
z
L
.
x
z
))
latex
Definitions
||
as
||
,
l
[
i
]
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
x
L
.
P
(
x
)
,
Prop
,
x
.
t
(
x
)
,
S
T
,
P
Q
,
P
Q
,
sorted(
L
)
,
True
,
T
,
,
hd(
l
)
,
i
<
j
,
i
j
,
A
&
B
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
{
T
}
,
SQType(
T
)
,
P
Q
,
Dec(
P
)
Lemmas
select
member
,
decidable
int
equal
,
l
member
wf
,
squash
wf
,
true
wf
,
select
cons
tl
,
int
seg
wf
,
select
wf
,
l
all
wf
,
le
wf
,
length
wf1
origin
T:Type. T 
(x:T, L:T List. sorted(x.L) 
sorted(L) & (z
L. x
z)) T:Type. T (x:T, L:T List. sorted(x.L) sorted(L) & (zL. xz)) Q
AB j < k
}x:A. B(x) TxL. P(x)
x. t(x) T Q Q
T
jj
x:A. B(x) l)
Q